E:Type{i}, pred?:(E(E+Unit)), X1, X2:Type{i}, info:(E(IdX1+(IdLnkE)X2)).
EOrderAxioms{i}(E;  pred?;info)  Prop{i'} 

latex

Definitions	t  T, Unit, IdLnk, Id, x:A. B(x), e < e', P  Q, sender(e), Prop, link(e), rcv?(e), b, source(l), loc(e), P & Q, pred(e), first(e), A, pred!(e;e'), x,y. t(x;y), SWellFounded(R(x;y)), destination(l), P  Q, x:A. B(x), EOrderAxioms(E; pred?; info)
Lemmas	ldst wf, strongwellfounded wf, pred! wf, not wf, first wf, pred wf, loc wf, lsrc wf, assert wf, rcv? wf, link wf, sender wf, cless wf, Id wf, IdLnk wf, unit wf